It is well known that the length of a beta-reduction sequence of a simplytyped lambda-term of order k can be huge; it is as large as k-fold exponentialin the size of the lambda-term in the worst case. We consider the followingrelevant question about quantitative properties, instead of the worst case: howmany simply typed lambda-terms have very long reduction sequences? We provide apartial answer to this question, by showing that asymptotically almost everysimply typed lambda-term of order k has a reduction sequence as long as(k-1)-fold exponential in the term size, under the assumption that the arity offunctions and the number of variables that may occur in every subterm arebounded above by a constant. To prove it, we have extended the infinite monkeytheorem for strings to a parametrized one for regular tree languages, which maybe of independent interest. The work has been motivated by quantitativeanalysis of the complexity of higher-order model checking.
展开▼
